YES 11.099
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (\vv1 ->
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\vv1→
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices0 | p vv1 | =
case | vv1 of | | (x,i) | → if p x then i : [] else [] |
| _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = |
case | vv1 of |
| (x,i) | -> | if p x then i : [] else [] |
| _ | -> | [] |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Case Reductions:
The following Case expression
case | vv1 of |
| (x,i) | → if p x then i : [] else [] |
| _ | → [] |
is transformed to
findIndices00 | p (x,i) | = if p x then i : [] else [] |
findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | if p x then i : [] else [] |
findIndices00 | p _ | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
findIndices000 | i True | = i : [] |
findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p _ | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
mainModule List
| ((elemIndices :: Float -> [Float] -> [Int]) :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule List
| (elemIndices :: Float -> [Float] -> [Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| elemIndices :: Eq a => a -> [a] -> [Int]
elemIndices | x | = | findIndices (== x) |
|
| findIndices :: (a -> Bool) -> [a] -> [Int]
findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
|
findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
|
findIndices00 | p (x,i) | = | findIndices000 i (p x) |
findIndices00 | p vw | = | [] |
|
|
findIndices000 | i True | = | i : [] |
findIndices000 | i False | = | [] |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(wy5100), Succ(wy400000)) → new_primPlusNat(wy5100, wy400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(wy5100), Succ(wy400000)) → new_primPlusNat(wy5100, wy400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(wy3100), Succ(wy40100)) → new_primMulNat(wy3100, Succ(wy40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(wy3100), Succ(wy40100)) → new_primMulNat(wy3100, Succ(wy40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs(wy121, Succ(wy17800), Succ(wy22300), wy222) → new_psPs(wy121, wy17800, wy22300, wy222)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(wy121, Succ(wy17800), Succ(wy22300), wy222) → new_psPs(wy121, wy17800, wy22300, wy222)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Succ(wy1800), wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs1(wy123, Succ(wy1800), wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Succ(wy1790), wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Succ(wy1790), wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(wy310, :(wy4110, wy4111), wy123) → new_foldr0(wy310, wy4110, wy4111, new_primPlusNat0(wy123, Succ(Zero)), new_primPlusNat0(wy123, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr0(wy310, Float(Neg(wy41000), wy4101), wy411, wy124, wy123) → new_psPs1(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_foldr0(wy310, Float(Pos(wy41000), wy4101), wy411, wy124, wy123) → new_psPs0(wy123, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_psPs0(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs0(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs1(wy123, Zero, wy310, Neg(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs1(wy123, Zero, wy310, Pos(wy41010), wy411) → new_foldr(wy310, wy411, wy123)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs2(wy141, Succ(wy1830), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr1(wy43, wy410, :(wy4410, wy4411), wy141) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_psPs3(wy141, Succ(wy1840), wy410, Pos(wy44010), wy43, :(wy4410, wy4411)) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_foldr2(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy142, wy141) → new_psPs3(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs2(wy141, Succ(wy1830), wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr2(wy43, wy410, Float(Pos(wy44000), wy4401), wy441, wy142, wy141) → new_psPs2(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs3(wy141, Succ(wy1840), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs2(wy141, Succ(wy1830), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr1(wy43, wy410, :(wy4410, wy4411), wy141) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_psPs3(wy141, Succ(wy1840), wy410, Pos(wy44010), wy43, :(wy4410, wy4411)) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
new_foldr2(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy142, wy141) → new_psPs3(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs2(wy141, Succ(wy1830), wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_foldr2(wy43, wy410, Float(Pos(wy44000), wy4401), wy441, wy142, wy141) → new_psPs2(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
new_psPs3(wy141, Succ(wy1840), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs2(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
new_psPs3(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr1(wy43, wy410, :(wy4410, wy4411), wy141) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
- new_foldr2(wy43, wy410, Float(Pos(wy44000), wy4401), wy441, wy142, wy141) → new_psPs2(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_foldr2(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy142, wy141) → new_psPs3(wy141, new_primMulNat0(Succ(wy43), wy44000), wy410, wy4401, wy43, wy441)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_psPs3(wy141, Succ(wy1840), wy410, Pos(wy44010), wy43, :(wy4410, wy4411)) → new_foldr2(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy141, Succ(Zero)), new_primPlusNat0(wy141, Succ(Zero)))
The graph contains the following edges 5 >= 1, 3 >= 2, 6 > 3, 6 > 4
- new_psPs3(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs3(wy141, Succ(wy1840), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs3(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wy141, Succ(wy1830), wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wy141, Succ(wy1830), wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wy141, Zero, wy410, Neg(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs2(wy141, Zero, wy410, Pos(wy44010), wy43, wy441) → new_foldr1(wy43, wy410, wy441, wy141)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Succ(wy1750), wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Succ(wy1760), wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
new_psPs4(wy119, Succ(wy1750), wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Succ(wy1760), wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat1(Zero, x0)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr3(wy310, :(wy4110, wy4111), wy119) → new_foldr4(wy310, wy4110, wy4111, new_primPlusNat0(wy119, Succ(Zero)), new_primPlusNat0(wy119, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr4(wy310, Float(Neg(wy41000), wy4101), wy411, wy120, wy119) → new_psPs5(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_foldr4(wy310, Float(Pos(wy41000), wy4101), wy411, wy120, wy119) → new_psPs4(wy119, new_primMulNat0(Zero, wy41000), wy310, wy4101, wy411)
The graph contains the following edges 5 >= 1, 1 >= 3, 2 > 4, 3 >= 5
- new_psPs4(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs4(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs5(wy119, Zero, wy310, Neg(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
- new_psPs5(wy119, Zero, wy310, Pos(wy41010), wy411) → new_foldr3(wy310, wy411, wy119)
The graph contains the following edges 3 >= 1, 5 >= 2, 1 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr6(wy310, wy4110, wy4111, wy221, wy220) → new_foldr5(wy310, wy4111, wy220)
new_foldr5(wy310, :(wy4110, wy4111), wy125) → new_foldr6(wy310, wy4110, wy4111, new_primPlusNat0(wy125, Succ(Zero)), new_primPlusNat0(wy125, Succ(Zero)))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr5(wy310, :(wy4110, wy4111), wy125) → new_foldr6(wy310, wy4110, wy4111, new_primPlusNat0(wy125, Succ(Zero)), new_primPlusNat0(wy125, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr6(wy310, wy4110, wy4111, wy221, wy220) → new_foldr5(wy310, wy4111, wy220)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr8(wy43, wy410, Float(Pos(wy44000), wy4401), :(wy4410, wy4411), wy144, wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))
new_foldr8(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy144, wy143) → new_foldr7(wy43, wy410, wy441, wy143)
new_foldr7(wy43, wy410, :(wy4410, wy4411), wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr8(wy43, wy410, Float(Pos(wy44000), wy4401), :(wy4410, wy4411), wy144, wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_foldr8(wy43, wy410, Float(Neg(wy44000), wy4401), wy441, wy144, wy143) → new_foldr7(wy43, wy410, wy441, wy143)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_foldr7(wy43, wy410, :(wy4410, wy4411), wy143) → new_foldr8(wy43, wy410, wy4410, wy4411, new_primPlusNat0(wy143, Succ(Zero)), new_primPlusNat0(wy143, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr10(wy310, Float(Neg(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)
new_foldr9(wy310, :(wy4110, wy4111), wy121) → new_foldr10(wy310, wy4110, wy4111, new_primPlusNat0(wy121, Succ(Zero)), new_primPlusNat0(wy121, Succ(Zero)))
new_foldr10(wy310, Float(Pos(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr9(wy310, :(wy4110, wy4111), wy121) → new_foldr10(wy310, wy4110, wy4111, new_primPlusNat0(wy121, Succ(Zero)), new_primPlusNat0(wy121, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
- new_foldr10(wy310, Float(Neg(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
- new_foldr10(wy310, Float(Pos(wy41000), wy4101), wy411, wy122, wy121) → new_foldr9(wy310, wy411, wy121)
The graph contains the following edges 1 >= 1, 3 >= 2, 5 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldr11(wy80, wy780, :(wy8110, wy8111), wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
new_foldr12(wy80, wy780, Float(Pos(wy81000), wy8101), :(wy8110, wy8111), wy174, wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
new_foldr12(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy174, wy173) → new_foldr11(wy80, wy780, wy811, wy173)
The TRS R consists of the following rules:
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr12(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy174, wy173) → new_foldr11(wy80, wy780, wy811, wy173)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_foldr12(wy80, wy780, Float(Pos(wy81000), wy8101), :(wy8110, wy8111), wy174, wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_foldr11(wy80, wy780, :(wy8110, wy8111), wy173) → new_foldr12(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy173, Succ(Zero)), new_primPlusNat0(wy173, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs6(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy172, wy171) → new_psPs7(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Succ(wy1860), wy780, Pos(wy81010), wy80, :(wy8110, wy8111)) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_foldr13(wy80, wy780, :(wy8110, wy8111), wy171) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_psPs7(wy171, Succ(wy1870), wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs6(wy171, Succ(wy1860), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Pos(wy81000), wy8101), wy811, wy172, wy171) → new_psPs6(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Succ(wy1870), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The TRS R consists of the following rules:
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs6(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy172, wy171) → new_psPs7(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Succ(wy1860), wy780, Pos(wy81010), wy80, :(wy8110, wy8111)) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_foldr13(wy80, wy780, :(wy8110, wy8111), wy171) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
new_psPs7(wy171, Succ(wy1870), wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs6(wy171, Succ(wy1860), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_foldr14(wy80, wy780, Float(Pos(wy81000), wy8101), wy811, wy172, wy171) → new_psPs6(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
new_psPs6(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
new_psPs7(wy171, Succ(wy1870), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The TRS R consists of the following rules:
new_primMulNat0(Succ(wy3100), Zero) → Zero
new_primMulNat0(Succ(wy3100), Succ(wy40100)) → new_primPlusNat1(new_primMulNat0(wy3100, Succ(wy40100)), wy40100)
new_primMulNat0(Zero, Succ(wy40100)) → Zero
new_primPlusNat1(Zero, wy40000) → Succ(wy40000)
new_primPlusNat1(Succ(wy510), wy40000) → Succ(Succ(new_primPlusNat0(wy510, wy40000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(wy5100), Zero) → Succ(wy5100)
new_primPlusNat0(Zero, Succ(wy400000)) → Succ(wy400000)
new_primPlusNat0(Succ(wy5100), Succ(wy400000)) → Succ(Succ(new_primPlusNat0(wy5100, wy400000)))
The set Q consists of the following terms:
new_primMulNat0(Zero, Succ(x0))
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat1(Succ(x0), x1)
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Succ(x0), Succ(x1))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Zero, Zero)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr13(wy80, wy780, :(wy8110, wy8111), wy171) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4
- new_foldr14(wy80, wy780, Float(Pos(wy81000), wy8101), wy811, wy172, wy171) → new_psPs6(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_foldr14(wy80, wy780, Float(Neg(wy81000), wy8101), wy811, wy172, wy171) → new_psPs7(wy171, new_primMulNat0(Succ(wy80), wy81000), wy780, wy8101, wy80, wy811)
The graph contains the following edges 6 >= 1, 2 >= 3, 3 > 4, 1 >= 5, 4 >= 6
- new_psPs6(wy171, Succ(wy1860), wy780, Pos(wy81010), wy80, :(wy8110, wy8111)) → new_foldr14(wy80, wy780, wy8110, wy8111, new_primPlusNat0(wy171, Succ(Zero)), new_primPlusNat0(wy171, Succ(Zero)))
The graph contains the following edges 5 >= 1, 3 >= 2, 6 > 3, 6 > 4
- new_psPs7(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wy171, Succ(wy1870), wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs7(wy171, Succ(wy1870), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wy171, Zero, wy780, Pos(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wy171, Succ(wy1860), wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4
- new_psPs6(wy171, Zero, wy780, Neg(wy81010), wy80, wy811) → new_foldr13(wy80, wy780, wy811, wy171)
The graph contains the following edges 5 >= 1, 3 >= 2, 6 >= 3, 1 >= 4